|
1: |
|
minus(x,0) |
→ x |
2: |
|
minus(s(x),s(y)) |
→ minus(x,y) |
3: |
|
quot(0,s(y)) |
→ 0 |
4: |
|
quot(s(x),s(y)) |
→ s(quot(minus(x,y),s(y))) |
5: |
|
app(nil,y) |
→ y |
6: |
|
app(add(n,x),y) |
→ add(n,app(x,y)) |
7: |
|
reverse(nil) |
→ nil |
8: |
|
reverse(add(n,x)) |
→ app(reverse(x),add(n,nil)) |
9: |
|
shuffle(nil) |
→ nil |
10: |
|
shuffle(add(n,x)) |
→ add(n,shuffle(reverse(x))) |
11: |
|
concat(leaf,y) |
→ y |
12: |
|
concat(cons(u,v),y) |
→ cons(u,concat(v,y)) |
13: |
|
less_leaves(x,leaf) |
→ false |
14: |
|
less_leaves(leaf,cons(w,z)) |
→ true |
15: |
|
less_leaves(cons(u,v),cons(w,z)) |
→ less_leaves(concat(u,v),concat(w,z)) |
|
There are 12 dependency pairs:
|
16: |
|
MINUS(s(x),s(y)) |
→ MINUS(x,y) |
17: |
|
QUOT(s(x),s(y)) |
→ QUOT(minus(x,y),s(y)) |
18: |
|
QUOT(s(x),s(y)) |
→ MINUS(x,y) |
19: |
|
APP(add(n,x),y) |
→ APP(x,y) |
20: |
|
REVERSE(add(n,x)) |
→ APP(reverse(x),add(n,nil)) |
21: |
|
REVERSE(add(n,x)) |
→ REVERSE(x) |
22: |
|
SHUFFLE(add(n,x)) |
→ SHUFFLE(reverse(x)) |
23: |
|
SHUFFLE(add(n,x)) |
→ REVERSE(x) |
24: |
|
CONCAT(cons(u,v),y) |
→ CONCAT(v,y) |
25: |
|
LESS_LEAVES(cons(u,v),cons(w,z)) |
→ LESS_LEAVES(concat(u,v),concat(w,z)) |
26: |
|
LESS_LEAVES(cons(u,v),cons(w,z)) |
→ CONCAT(u,v) |
27: |
|
LESS_LEAVES(cons(u,v),cons(w,z)) |
→ CONCAT(w,z) |
|
The approximated dependency graph contains 7 SCCs:
{19},
{24},
{25},
{16},
{17},
{21}
and {22}.